package com.googlecode.kipler.satisfiability.completion.rule.individual;

import java.util.HashSet;
import java.util.Iterator;
import java.util.Set;

import com.googlecode.kipler.container.dl.ABox;
import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.Individual;
import com.googlecode.kipler.container.dl.SHOIQABox;
import com.googlecode.kipler.container.dl.SHOIQIndividual;
import com.googlecode.kipler.container.dl.WcsData;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.container.dl.operational.SHOIQAncestorCollector;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;
import com.googlecode.kipler.syntax.Role;
import com.googlecode.kipler.syntax.formula.SameIndividualAssertion;


/**
 * 
 * @author İnanç Seylan
 * 
 */
public class SHOIQMergeStrategy implements MergeStrategy {
	private SHOIQABox aBox;

	private DependencySet dependedWcs = new DependencySet();

	private SHOIQABox getABox() {
		return aBox;
	}

	private void setABox(ABox abox) {
		this.aBox = (SHOIQABox) abox;
	}

	private DependencySet getDependencySet() {
		return dependedWcs;
	}

	private void setDependencySet(DependencySet dependedWcs) {
		this.dependedWcs = dependedWcs;
	}

	public MergePair choosePair(ABox aBox, Set<Individual> neighbors) {
		setABox(aBox);
		MergePair result = null;
		Iterator<Individual> i = neighbors.iterator();
		while (i.hasNext() && result == null) {
			Individual x = i.next();
			Iterator<Individual> j = neighbors.iterator();
			while (j.hasNext() && result == null) {
				Individual y = j.next();
				SameIndividualAssertion ia = new SameIndividualAssertion(x
						.getName(), y.getName()).toggleNegated();
				if (x != y && !getABox().contains(ia)) {
					if (getABox().isNominal(x)) {
						result = new MergePair(y.getName(), x.getName());
					} else if (getABox().isNominal(y)
							|| new SHOIQAncestorCollector(getABox(), x)
									.collect().contains(y)) {
						result = new MergePair(x.getName(), y.getName());
					} else {
						result = new MergePair(y.getName(), x.getName());
					}
				}
			}
		}
		return result;
	}

	// TODO: try to find a way to remove "owner" from this method's interface.
	public void merge(String owner, ABox aBox, MergePair pair,
			DependencySet dependencySet)
			throws UnsatisfiableException {
		setABox(aBox);
		setDependencySet(dependencySet);
		WorldConstraintSystem wcs = getABox().getWorld().getWcs();
		wcs.getData().getLogger().info(
				"WCS " + wcs.getId() + " SHOIQ merging " + pair.getFrom()
						+ " into " + pair.getInto());
		SHOIQIndividual x = (SHOIQIndividual) getABox().getIndividual(
				pair.getInto());
		SHOIQIndividual y = (SHOIQIndividual) getABox().getIndividual(
				pair.getFrom());
		moveZYEdgesToX(y, x);
		moveYZEdgesToX(y, x);
		MergeUtility mergeUtility = new MergeUtility(getABox(),
				getDependencySet());
		mergeUtility.mergeConcepts(y.getName(), x.getName());
		mergeUtility.mergeInequalities(y.getName(), x.getName());
		/*
		 * if both x and y are blockable, then x's level is still UNKNOWN; if
		 * one of x or y is nominal and the other blockable, then x's level is
		 * that of the nominal node; if both x and y are nominals, then x's
		 * level is the minimum of x and y's levels.
		 */
		x.setLevel(Math.min(x.getLevel(), y.getLevel()));
		prune(getABox(), y.getName());
		manageModifiedIndividuals(pair);
	}

	private void manageModifiedIndividuals(MergePair pair) {
		WcsData wcsData = getABox().getWorld().getWcs().getData();
		wcsData.getModifiedIndividuals().replace(
				getABox().getWorld().getName(), pair.getFrom(), pair.getInto());
	}

	public void prune(ABox aBox, String indvName) {
		setABox(aBox);
		Set<Individual> toBePrunedSet = new HashSet<Individual>();
		collectPruneNodes(indvName, toBePrunedSet);
		for (Individual indv : toBePrunedSet) {
			getABox().remove(indv.getName());
		}
	}

	private void collectPruneNodes(String indvName,
			Set<Individual> toBePrunedSet) {
		Individual indv = getABox().getIndividual(indvName);
		toBePrunedSet.add(indv);
		Iterator<Individual> i = aBox.successorIterator(indv);
		while (i.hasNext()) {
			Individual successor = i.next();
			if (getABox().isBlockable(successor)) {
				collectPruneNodes(successor.getName(), toBePrunedSet);
			}
		}
	}

	/**
	 * @param y
	 * @param x
	 * @throws UnsatisfiableException
	 */
	private void moveYZEdgesToX(Individual y, Individual x)
			throws UnsatisfiableException {
		MergeUtility mergeUtility = new MergeUtility(getABox(),
				getDependencySet());
		Iterator<Individual> i = aBox.successorIterator(y);
		while (i.hasNext()) {
			Individual z = i.next();
			if (getABox().isNominal(z)) {
				if (!aBox.containsEdge(z, x) || aBox.containsEdge(x, z)) {
					for (Role role : aBox.getEdges(y, z)) {
						mergeUtility.mergeEdge(role, y, z, role, x, z);
					}
				}
				if (aBox.containsEdge(z, x)) {
					for (Role role : aBox.getEdges(y, z)) {
						Role invRole = role.copy().toggleInverse();
						mergeUtility.mergeEdge(role, y, z, invRole, z, x);
					}
				}
			}
			/*
			 * "remove (y,z) from E". When y is removed by the ABox.remove()
			 * method, (y, z) will also be removed from E.
			 */
		}
	}

	/**
	 * @param y
	 * @param x
	 * @throws UnsatisfiableException
	 */
	private void moveZYEdgesToX(Individual y, Individual x)
			throws UnsatisfiableException {
		MergeUtility mergeUtility = new MergeUtility(getABox(),
				getDependencySet());
		Iterator<Individual> i = aBox.predecessorIterator(y);
		while (i.hasNext()) {
			Individual z = i.next();
			if (!aBox.containsEdge(x, z) || aBox.containsEdge(z, x)) {
				for (Role role : aBox.getEdges(z, y)) {
					mergeUtility.mergeEdge(role, z, y, role, z, x);
				}
			}
			if (aBox.containsEdge(x, z)) {
				for (Role role : aBox.getEdges(z, y)) {
					Role invRole = role.copy().toggleInverse();
					mergeUtility.mergeEdge(role, z, y, invRole, x, z);
				}
			}
			/*
			 * "remove (z,y) from E". When y is removed by the ABox.remove()
			 * method, (z, y) will also be removed from E.
			 */
		}
	}

}
